Sphincs aggregation - #18

Given a lifetime and a budget for keygen, signing (vanilla and half-top
cached) and signature size, search.py enumerates the parameter space and
reports the sets minimizing verification cost at NIST level 1 (128-bit
classical, the SLH-DSA level 1 target).

Two axes need no enumerating, which is what keeps this in Python:

- k is determined by (h, a). The forgery exponent is increasing in k while
  size, signing and verification all grow with it, so only the smallest
  secure k is ever worth costing: a cached binary search, not an axis.
- S_wn likewise. Verification is strictly decreasing in it and the grinding
  is increasing above the mean, so the answer is the largest S_wn whose
  grinding still fits the signing budgets.

What is left is (scheme, h, d | h, chain_bits, dropped_chains, a), pruned by
keygen before a and by size and signing before S_wn. On the default grid the
loose-budget worst case is ~70k grid tuples and ~2M cost-model calls, 20s;
realistic budgets prune to a few seconds, so a Rust port is not needed.

--selftest checks both shortcuts rather than trusting them: that the
digit-sum count is unimodal with its peak at the mean (so the S_wn search
cannot skip a larger admissible sum), that min_secure_k matches a linear
scan, and that on a grid small enough to exhaust, the pruned search returns
the same optimum as a sweep over every k and every S_wn.

Cross-check: given budgets near the report's 2^40 numbers and its grid
(w in {16, 256}, no chain dropping), the search rediscovers its bold row,
h=40 d=5 a=14 k=11 w=256, and then spends the leftover signing budget by
raising S_wn from 2040 to 2882, which cuts verification from 10,402 hashes
to 6,190.

sphincs_params.py grows a costs() that returns everything not depending on
q_s, with evaluate() as costs() plus the security level, so the search pays
0.23ms for a security sum only when it needs one rather than on every one of
two million candidates.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Replaces the two python scripts with a dependency-free cargo project in its
own workspace. The point of the port is not speed for its own sake: it buys
enough of it that the search needs no cleverness at all.

The python search leaned on two monotonicity arguments to stay tractable:
only the smallest secure k was ever costed, and the target sum was reached by
binary search. Both are provable, but both had to be trusted. Here every
(scheme, h, d | h, chain_bits, dropped_chains, a, k, S_wn) point is costed
and compared. The three tests that run before the target-sum scan reject only
points no target sum could rescue: size and keygen do not depend on the
target sum at all, and the least grinding any target sum can ask for is read
off the digit-sum table rather than assumed to sit at the mean.

That table is the other reason this is affordable. nu is now the coefficient
vector of (1+x+..+x^(w-1))^l, built once per (l, w) by convolution, u128
throughout because every coefficient is bounded by the total w^l <= 2^128.
The report's inclusion-exclusion formula needs bignums for intermediates
that dwarf their own result, and it was what made the python inner loop slow.

Costs come out identical to the python, which came out identical to the sage
scripts. The 2^30 query lands on the same winner in 4.3s against 61s, having
costed 150M parameter sets rather than 2.5M; the query with budgets so loose
that nothing prunes evaluates 3.7 billion feasible points in 24s, where the
fully exhaustive python would have run for hours. No threads.

Search ranges are now hardcoded constants (h <= 96, a <= 32, k <= 64,
chain_bits <= 12, dropped <= 16), wide enough that the budgets normally bind.
When a winner comes out at the top of one, the run says so and names the
constant to raise, since there the range and not the budget may be what is
limiting the answer.

Two bugs found in the port, neither present in the python:
- ceil(2^128 / nu) carried its +1 past u128 when nu = 1, wrapping to zero, so
  the maximal target sum looked free to grind and won every comparison.
- 1u64 << h' masks the shift rather than overflowing, so h = 64, d = 1
  reported the keygen of a one-leaf tree. Trees that do not fit a u64 count
  are now rejected, which no budget expressible in a u64 could admit anyway.

tests/goldens.rs carries every fixture the python had: the upstream sage
fixtures under both hash conventions, all 18 WOTS/FORS rows of the report's
Tables 1 and 2, the doc/xmss digest-cut geometry, exact nu values, thirteen
security levels against the 100-digit decimal sum (the f64 log2-space sum
here agrees to under a thousandth of a bit), and the search against a naive
oracle that skips nothing, tuple by tuple rather than just on the winner.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The hypertree no longer splits h uniformly. The top tree takes h_top and the
layers below divide what is left as evenly as it goes, so d need not divide h.

This pays because of an asymmetry the uniform split hides. The signature
carries h authentication nodes and the verifier walks them however the layers
divide h, so size and verification depend only on (h, d), not on the split.
Keygen depends only on h_top, and signing sums 2^height over the layers. Only
the top tree is cacheable, and it pays sqrt there. So height moved into the
top layer is free on the objective, costs keygen and vanilla signing, and buys
cached signing: at h=40, d=5, h_top=15 against the uniform 8 leaves the
signature and its 10402-hash verification untouched while cached signing goes
4.79M -> 2.36M hashes, keygen 1.05M -> 134M once.

Dropping d | h pays on its own. On the report's 2^40 budgets and grid the
search now prefers h=39, d=5 with heights 8+8+8+8+7 over h=40, d=5: 16 bytes
and one auth node cheaper, which buys enough grinding budget to raise the
target sum, and verification falls 6190 -> 5660 hashes. On the 2^30 query the
winner moves to h=34, d=3 with heights 12+11+11 and 674 verification hashes
against 751, at 3916 bytes against 3996.

Only "top one, then the rest equal" is enumerated, which is not a restriction:
for a fixed (h, d, h_top) that shape matches every other on size, verification
and keygen, and beats them on both signing costs, because a sum of 2^height at
fixed total is smallest when the heights are equal. So (h, d, h_top) covers
the cost-optimal representative of every layer profile.

The new axis costs nothing in the inner loop. Which h_top is best does not
depend on (a, k) or on the target sum, because both signing budgets take the
(a, k) part as the same additive offset, so the profiles are ranked once per
(h, d) by the grinding they leave room for and that ranking holds throughout.
Params splits into Layers (the hypertree) and Skeleton (the FORS side, the
size and the verifier), which is what makes the two independent in code as
well. The realistic 2^30 query is 2.0s, down from 4.3s, over a grid 5.6x
larger, because ranking profiles by keygen rejects (h, d) pairs sooner.

Two things found while wiring it up: the row list needed a bound, since
budgets loose enough to admit 12M rows would hold 3GB to print a dozen (now
121MB, with the stats line reporting what was dropped as worse than everything
kept), and the dedup map was dead weight because each parameter tuple is
reached exactly once. The naive oracle sweeps h_top too, so the goldens still
diff the search against something that skips nothing.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Leaves doc/sphincs/ free for whatever else belongs to the scheme, the way
doc/leanvm/ and doc/xmss/ hold their own specs. Pure move: same crate, same
numbers, one path in the README and one in AGENTS.md.

Replaces the params/search subcommands with a single invocation. Every flag is
optional: giving a parameter pins it, leaving it out searches it, and pinning
them all is how one set gets costed. Budgets are optional too, an unset one
being no limit, so the two old behaviours are the two ends of one dial rather
than two code paths.

That needed a rule for the axes that only ever trade signer work for cheaper
verification, since with nothing bounding the signer they are unbounded and
their answer is useless: left free and unbudgeted, the first run of this
dropped 5 WOTS+C chains and ground 10^20 counters to reach 4.03K verification
hashes. So the target sum, the dropped chains and the top height take the
value the report's own sets use when nothing bounds the signer, and are
searched as soon as a budget does. That makes the fully pinned command
reproduce the report's bold 2^40 row exactly, 4356 bytes and 10402 hashes,
with no table around it.

Grid axes are now Spans (pinned when lo == hi), h_top an Option<Span> because
"the classic h/d split" is not a value it can hold, and budgets are Options so
an unset one neither constrains nor gets a percentage in the utilization line.
The table only prints when there is more than one row.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

sign$ and state were shorthand only I could read. They are now `cached` and
`cache B`, and the table carries a two-line legend for the columns that are
this project's own rather than the report's: the top layer height, the two
signing costs and the state one of them assumes, and which unit everything
is in.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Drops the hashes/compressions unit switch and the FIPS 205 SHA-2 layout it
selected between. There is one rule now: a hash of P (n bytes), a tweak (n
bytes) and a payload costs ceil((2n + payload) / 64) compression calls, since
both BLAKE2s and the length-prefixed SHA-256 of primitives::sha2 absorb 64
bytes per call and spend nothing on padding.

At n = 16 that is one compression for a Merkle node (two 16-byte children fill
a block exactly) and one for a WOTS chain step, two for the message digest
(doc/xmss's IncEnc hashes 32 bytes of prefix, a 32-byte message, 24 bytes of
randomness and 8 of padding), and ceil((32 + 16m) / 64) for compressing m hash
values.

It changes no number. That rule and the report's ceil((22*8 + 128m + 65)/512)
are the same function for every m from 1 to 4000, checked as a golden, so the
sage fixtures still pin the model and the report's compression columns are
still the yardstick. The hash counts stay in Cost, unreported, only so the 18
WOTS/FORS rows of the report's Tables 1 and 2 can keep checking a second
projection of the same walk.

The report and the search table now carry one column instead of two, budgets
are compressions without saying so at every mention, and the grinding line
reports what grinding costs rather than how many trials it takes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Same syntax as the budgets, so 16e6 means sixteen million signatures. The
security sum never needed q_s to be a power of two: it carries the binomial
term by its recurrence, so an f64 count works everywhere the log2 did, and
non-power-of-two lifetimes are now expressible at all.

Reported back as 2^40 when it is a power of two and as 16.000M (2^23.9) when
it is not.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

It still read --lifetime 24, which under a signature count means twenty-four
signatures. My rewrite matched the literal 30 that used to be there and so
changed nothing. 16e6 is the same lifetime 24 meant as a log.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

There is one signing budget now, --max-sign, and it counts signing with the
top XMSS tree's half top already in state: the steady-state cost of a signer
that keeps the cache, which is the cost worth optimizing. The old --max-sign,
which rebuilt every tree from the seed, is now reported as `cold` and budgeted
by nothing, since a signer only pays it once after restoring a backup.

Costs.sign is therefore the cached figure and Costs.sign_cold the other one,
which is also the projection the upstream sage scripts compute: they have no
cache notion, so the fixtures and the report's SigTime column now pin
sign_cold.

Gating the three spend-to-save axes gets more precise with one budget instead
of two. --swn and --drop-chains buy cheaper verification with grinding, so
they follow --max-sign; --top-height buys cheaper signing with key generation
and cold signing, so it follows --max-keygen. Before, a --max-sign with no
--max-keygen would have searched top heights against a keygen cost nothing
bounded.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

100,000 and 100_000 now parse alongside 2e6, wherever a number is taken.

Unknown flags were silently dropped, so a command line carrying a flag from
before a rename ran anyway with that constraint quietly missing. They are an
error now, and the ones this tool used to have name their replacement:
--max-sign-cached points at --max-sign, --unit and --uncached at there being
one unit, --max-dropped at --drop-chains, and --h-max and friends at the
constants in src/search.rs, which is where a wider range now comes from. The
edges warning was still telling people to raise a flag that no longer widens
anything, and says the constant instead.

When nothing is feasible the run now says what rejected things, counting the
layer sets over --max-keygen, the parameter sets over --max-size and over
--max-sign, and the (a, k) pairs that never reached the security floor. It
used to guess that size or keygen was to blame, which for a tight signing
budget is the wrong pointer.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

cb was log2(w), which is what doc/xmss/main.tex calls w and what the report
calls log w, so the column was ambiguous whichever way it was read. It shows
the Winternitz parameter itself now, matching -w and the report's tables, with
--chain-bits still taking the log on input.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Gone from the table and from the per-set report. It stays in Costs, unreported
like the hash counts, because it is the projection the upstream sage scripts
compute, having no cache notion, and so is what tests/goldens checks their
fixtures and the report's SigTime column against.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The table was suppressed whenever there was one row, which conflated two
different runs: one where every axis was pinned, where a bare report is
exactly right, and a search so tightly budgeted that only one parameter tuple
survives, where a bare report looks like the search never happened. A budget
of 100,000 compressions for signing is the second kind: 55.8M candidates fall
to it and one gets through.

The count and the table now follow whether anything was searched at all, which
Grid::fully_pinned answers, not how many rows came back. Also "1 feasible set"
rather than "1 feasible sets, best 1 by verification cost", and the stats line
counts parameter tuples rather than rows.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… shape

Profile now holds an arbitrary height vector, top first, so a hypertree with
heights 11 + 5 + 7 + 3 can be costed. --heights takes them on the command
line, pinning h and d with them, and Layers::from_profile is the library entry
point.

The search still builds only the canonical shape, the top tree at h_top and
the rest dividing what is left as evenly as it goes, and now proves that costs
nothing. profile_shape_is_never_beaten enumerates every composition of five
small (h, d) pairs, 2000-odd of them, and checks that against the canonical
profile with the same top height each one ties on signature size, on
verification and on keygen, and loses or ties on both signing costs. The
argument was already in Profile's docs; it is checked now.

Visible in a pair of runs: 11 + 5 + 7 + 3 and 11 + 5 + 5 + 5 both give 3872
bytes, 8.37K compressions to verify and 8.40M to generate, and the uneven one
signs at 1.38M against 1.09M.

Heights ride in a [u8; 32], since a height past 63 makes 2^height uncountable
anyway, so a fully general profile is the same size as the compact top-plus-two
form it replaces and nothing in the hot loop grew. The final report no longer
recomputes the winner's costs to apply --cache-height either: that rides in the
grid now, so what gets printed is what the search actually costed, which is
also what makes --heights print the heights it was given.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

An ht column was complete while every profile was the canonical shape, since
(h, d, h_top) determines it. It is not complete now that any heights can be
costed, and it was never easy to read: the reader had to divide h - ht over
d - 1 layers themselves.

The column carries the profile run-length encoded instead, 2x12 or 12+13 or
6+2x11 or 11+5+7+3, which is worth having even for canonical shapes. A
keygen-starved search makes the point: with --max-keygen 3e4 the winner is
6+2x11, the top layer the shortest of the three, because keygen pays for that
tree alone. An ht of 6 said nothing about the 11s.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Every layer now carries its own Winternitz parameter, target sum and dropped
chain count, not just its height. Layer says what that buys, --layer costs one
such hypertree outright, and --split-wots searches a separate instance for the
top layer.

The Lagrangian the search was going to need collapses, which is the useful
finding. Minimising sum_i [verify_i + L*size_i + M*sign_i] is separable, so
each layer takes its own argmin, and every layer below the top has an
identical cost function, since only the top tree is the cached one and only it
is what keygen pays for. So at most two distinct choices ever come back, ties
aside, and ties are between neighbouring heights, which the +-1 split already
spans. Enumerating that two-group family gives the same answers with no
duality gap and stays a brute force, so the naive oracle survives:
two_groups_against_every_per_layer_assignment checks it against every
per-layer assignment of four small hypertrees and finds no gap.

Whether per-layer WOTS is worth searching is a separate question, and the
answer so far is no. Size charges every layer the same l*n and verification
charges every layer its own walk, so the exchange rate between them is
identical everywhere and a uniform w is what a size budget wants: the walk
(2^(8n/l) - 1)*l is convex in l, so at a fixed total l an equal split is
cheapest. Only signing distinguishes the layers. On the keygen-starved query
where heights come out 6 + 11 + 11, --split-wots finds the uniform choice
still winning at 377 compressions, with the split variants at 379. The target
sums do differ by a step, 205 on the top layer against 204 below.

Costs are now assembled from per-layer sums, which meant splitting the model
along the seam that matters: hyper_cost adds up a hypertree once, Fors is the
FORS side, and assemble is arithmetic. The target sums are allocated by
building each hypertree's grinding frontier once, greedily merging the two
groups' marginal costs, and binary searching it per (a, k) rather than
rescanning.

Three things made the first working version 98s where the old one was 2s: a
NuTable cloned per candidate to dodge a borrow (NuCache::pair now hands out
two at once), a linear frontier scan, and the size prune losing its break.
That brought it to 14s, and rayon over the (scheme, WOTS instance) tasks to
2.1s, with the security table filled up front so the workers share it
read-only. --split-wots is 182 times the grid and takes minutes; the help says
so.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

This reverts commit 737c6d6. One WOTS instance for the whole hypertree again;
the layer heights still vary.

It never won, which the reverted commit's own numbers say: on the query where
the heights come out most uneven, 6 + 11 + 11 under a tight keygen budget,
--split-wots searched every pair of instances and the uniform choice still came
first at 377 compressions against 379. The one thing the split did buy was a
step of target sum on the top layer, 205 against 204, worth a single
compression on the 2^24 query. The reason is in the model rather than in those
queries: size charges every layer the same l*n and verification charges every
layer its own walk, so the exchange rate between them is identical everywhere,
and the walk is convex in l, so at a fixed total l an equal split is what a
size budget wants. Only signing distinguishes the layers.

So the axis was complexity for nothing: it doubled the searched grid per extra
instance, needed a grinding frontier per hypertree in place of a binary search,
and needed rayon to get back to the runtime it started at. Profile's docs now
say it was tried and why it lost, so nobody has to find out twice.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

# Conflicts:
#	AGENTS.md

…triangle

main.tex specifies the SPHINCS+ instance the parameter search picked: h = 26
over d = 3 layers of 12 + 7 + 7, a = 10, k = 15, w = 8, v = 42 chains at
target sum 191, no dropped chains, a 32-byte public key and a 4924-byte
signature. Written from first principles in the style of doc/xmss: the
tweakable hash and the tweak encoding, the index decomposition, then the
one-time signature, a layer, and the few-time signature as sub-algorithms, so
Sig and Ver are four steps each. Costs are counted in hash calls, 1.38M at key
generation, 190K per signature with 1024 bytes of cache, 497 at verification.
Security carries the strong-unforgeability game and nothing else yet; the
accounting and the quantum argument are TODO.

The signer's cache keeps only the 2^ceil(h_0/2) nodes of one level of layer
0's tree, not that level and everything above it: 1024 bytes rather than 2032,
paying 2^6 - 1 = 63 node calls per signature to refold the triangle above
them, against the 21,631 the subtree rebuild costs anyway. params_selection
models that unconditionally, so --cache-level-only is gone.

…gainst a review

formal/sphincs states, and does not prove, the classical random-oracle security of the
instance of doc/sphincs: `SphincsSecurityStatement`, which reads
`HasClassicalSecurityBits Concrete.scheme 120`. Everything the claim depends on is in
SphincsSecurity/Statement.lean, following formal/xmss: the parameters and types, the byte
layout of every hash input, the target-sum code, Gen, Sig and Ver as oracle computations,
then the game. The hash is a random oracle throughout; nothing instantiates it.

Three things differ from the XMSS statement, all because this scheme is stateless. A
signing request is a message with no epoch, so what the game caps is the number of signing
queries. Signing is randomized, so a message has many valid signatures and the game
rejects only one the signer actually returned, which is what makes this a strong
unforgeability claim. And the secret key holds the sampled secrets rather than precomputed
tables, because Gen builds only layer 0 and a replay cache would answer for queries it
never made, so signing rebuilds whatever tree it reads.

What the parameters fix about the layout is proven rather than asserted, next to the
definitions it concerns: the index decomposition for all 2^26 indices, and the
authentication path, which is where the flattening could have broken the scheme silently.
The claim is 120 and not 128 because the bound is a slope q/2^120 and every strategy costs
2^-128 per query, leaving 2^8 for the union bounds and constants a proof accumulates.

Three adversarial reviews found no attack and no vacuity: the summed per-query slopes are
2^-127.96, tweak injectivity holds over all ten families so no multi-target factor exists,
and an explicit admissible digest witnesses that Ver accepts. They corrected:

- the comparison to FIPS 205, whose default is the hedged variant and which derives R
  rather than sampling it, where the remark had it backwards;
- two "exactly when" claims, one-directional: a second admissible counter for the same
  codeword also recovers the leaf, so unforgeability on a signed message rests on
  collision resistance at tw_enc rather than on incomparability;
- the query count, now bounded on every execution path, with 2^58 named as where the claim
  is read;
- the win condition, which said "the signer's answer" for a message that can be signed
  more than once;
- k, labelled digest index groups rather than trees, and the node tweak ranges, which
  start at level 1;
- the refold count above the cached level, now an upper bound, 57 being exact since the
  triangle's root is never on a path;
- the few-time leak, a per-query slope of 2^-133.3 rather than a q-independent term, which
  is what fixes 2^24 signatures: it reaches 2^-120 at 2^26.4.

README.md records the two places a proof can go wrong, both found by attacking the claim
rather than reading it: the strong forgery branch above, and the one-step-lowering event,
which has 1258 exploitable codewords and so runs at 2^-117.7 per encoding query, above the
slope, and is a forgery only conjoined with a chain inversion.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Gen, Sig and Ver of doc/sphincs/main.tex, as a leaf crate over
primitives::hash, with no attempt yet to share the tweakable hash and
target-sum code with `xmss`.

Secrets are the seed-derived implementation of the specification's "Seed
derivation" remark, and a signer holds the 1024-byte layer-0 cache of its
"Signer state" remark: 64 nodes at depth 6, one 64-leaf subtree rebuilt
below them and 63 refolded above them per signature. Signing never builds
layer 0 whole, so key generation is the only place that does, and the
only place with any fan-out.

An instrumented build, not committed, counts the hash calls the cost
table claims: key generation 1384447 exactly (2^12 * 337 + 2^12 - 1),
verification 497 exactly on every signature, signing 186625 on average
over 40 signatures against the 189547 the table predicts, the gap being
one draw of three geometric counter searches of mean 12436. The ignored
`grinding_bits` test measures the two grinding loops at 2^13.61 and
2^9.98 attempts, against the specified 2^13.60 and 2^10.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Five conflicts, all in `rec_aggregation`, all where main touched what the
SPHINCS work rewrote.

main made `push_signature_hints` fallible: a raw signature whose
randomness does not decode to a target-sum encoding is now
`MalformedRawSignature` rather than a panic in the prover. Taken, and
propagated to the SPHINCS witness walk, which main could not know about:
`sphincs::encode` and `ots_leaf` were `.expect("a verified signature
encodes")` there and are now the same error, so neither scheme's malformed
input aborts where the other returns.

The statement conflicts resolve to this branch's two-list form, keeping
main's wording where it was the more precise of the two: the cap is
`strictly shorter than MAX_KEYS`, not "at most MAX_KEYS long", since the
check rejects at the cap. While there, `check_signer_set`'s doc stops
saying the lists' lengths count distinct signers: the XMSS one counts
distinct keys, the SPHINCS one distinct (key, message) claims.

main's two new tests are kept and extended rather than adapted away.
`max_keys_bound_is_exclusive` now also pins that the cap counts both
schemes, so `MAX_KEYS - 1` XMSS keys plus one SPHINCS claim is already
over, at both host checks. `malformed_raw_signature_is_an_error` gains a
SPHINCS counterpart, which is what pins the error path added above.

Everything else auto-merged: main's transcript, bus-root, Lagrange-window
and python-verifier work does not overlap the guest's SPHINCS code, whose
changes are confined to `main()`, the key-absorbing helpers and
`verify_sig_sphincs`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The security definition now has the shape `doc/xmss` settled on under
review: a $q$-bounded adversary, and `Pr[A wins] <= q / 2^x` rather than a
maximum of `Forge(q_s, q) / q` over $q$. The two say the same thing, the
second being the first unrolled, but the $q$-bounded form carries its
quantifier where a reader meets it, and with the `Forge` shape went the
sentence explaining that the claim is read past `q = 2^58`: that was an
artifact of dividing by $q$, not something about the scheme. What stays is
what makes this scheme's game different from the stateful one: no epoch, a
signing query capped at $\qs$ and repeatable on one message, since `Sig`
keeps no state, and a signature that may be $\bot$.

`formal/sphincs` is deleted, 1060 lines that stated a claim and proved
none of it. The security section is a target now, and says so; AGENTS.md
no longer sends a reader after a project that is not there. CI never built
it (`lean.yml` covers `formal/xmss` only), and its `Proof/` directory was
empty, so nothing unproven went with it that the history does not keep.

The target reads 127 bits at `2^24` signatures. That is tight for this
instance and worth knowing before anyone attempts it: the generic cost is
`2^-128` a query and the few-time leak `2^-133.3` at that many signatures,
which already sum to about `2^-127.9`, so a proof's union bounds and
constants have to be additively small against `2^-128` rather than
absorbed by slack.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

2709 lines that chose the instance rather than describing it: the security,
size and hash-count models, the search for the cheapest verification under
a budget, and the goldens pinning all of it against the Blockstream
project's sage fixtures. Its work is done, the instance it picked being
specified in `main.tex` and implemented in `crates/sphincs`, and it modelled
schemes this repo does not prove anything about, so keeping it in the tree
only invited the two to drift.

Kept on the `sphincs-params-search` branch, which is this commit's parent
with the directory intact, for whoever wants to move the parameters again.

It was a standalone cargo workspace, so nothing here built or tested it:
the root workspace takes `crates/*` only, and `doc.yml` reaches into
`doc/sphincs` for the LaTeX alone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>